The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

revApp#2(Nil, x16) → x16
revApp#2(Cons(x6, x4), x2) → revApp#2(x4, Cons(x6, x2))
dfsAcc#3(Leaf(x8), x16) → Cons(x8, x16)
dfsAcc#3(Node(x6, x4), x2) → dfsAcc#3(x4, dfsAcc#3(x6, x2))
main(x1) → revApp#2(dfsAcc#3(x1, Nil), Nil)

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3]
transitions:
Nil0() → 0
Cons0(0, 0) → 0
Leaf0(0) → 0
Node0(0, 0) → 0
revApp#20(0, 0) → 1
dfsAcc#30(0, 0) → 2
main0(0) → 3
Cons1(0, 0) → 4
revApp#21(0, 4) → 1
Cons1(0, 0) → 2
dfsAcc#31(0, 0) → 5
dfsAcc#31(0, 5) → 2
Nil1() → 7
dfsAcc#31(0, 7) → 6
Nil1() → 8
revApp#21(6, 8) → 3
Cons1(0, 4) → 4
Cons1(0, 5) → 2
Cons1(0, 0) → 5
Cons1(0, 7) → 6
dfsAcc#31(0, 5) → 5
dfsAcc#31(0, 7) → 5
dfsAcc#31(0, 5) → 6
Cons2(0, 8) → 9
revApp#22(7, 9) → 3
Cons1(0, 5) → 5
Cons1(0, 7) → 5
Cons1(0, 5) → 6
revApp#22(5, 9) → 3
Cons2(0, 9) → 9
revApp#22(0, 9) → 3
Cons1(0, 9) → 4
revApp#21(0, 4) → 3
0 → 1
4 → 1
4 → 3
9 → 3

(2) BOUNDS(1, n^1)